Did we ever experiment with using minimization to set globally?

I tried it, and some things fail. One big issue is that IsTrunc is not cumulative, since it is defined using IsTrunc_internal, which is a Fixpoint. As far as I know, fixpoints can't be made cumulative. So that means IsHProp and IsHSet are not cumulative, which causes problems. There are other issues as well. In one spot, the coercion equiv_fun needed to be manually inserted. In another, some types in generic universes were forced to be in Set. A large number of files compiled without problems, but I didn't keep pushing this to see how much breaks. I think it might just take a few hours to get something like this working, with some universe annotations to block the minimization to set when it causes problems.

The problem with IsHSet means that this PR needs updating. I'm just about to push a commit that frees up the proofs of IsHSet. While working on this, I noticed that Decidable and DecidablePaths are not cumulative. They are classes with a single field. These can be made cumulative if the field is surrounded by { and }, but then to construct instances, you need to use Build_Decidable everywhere, which is a bit awkward. So for now I have left them not cumulative, and have also freed up their proofs.

It would be easier to use minimization to Set widely if we could make more things cumulative somehow.

(I also just realized that Spaces/Nat.v could use a similar treatment. I'll take a look later today, so let's not merge this yet.)

We could consider making IsTrunc inductive rather than recursive.

Inductive IsTrunc : nat -> Type -> Type :=
| istrunc_iscontr : forall {A:Type}, IsContr A -> IsTrunc 0 A
| istrunc_succ : forall {A:Type} {n:nat}, (forall x y:A, IsTrunc n (x = y)) -> IsTrunc (S n) A.

Of course that would involve adding some constructors in places where now we can just compute.

We would probably want to change the argument order so that the type argument can be a parameter. Otherwise its universe has more restricted cumulativity AFAICT.

Ugh. Maybe we could make a notation that puts the arguments back in the right order.

It would be nice if there were a way to indicate which arguments are indices and which are parameters that didn't require all the parameters to come before all the indices.

@SkySkimmer Is there any chance that in the future Coq could have cumulative fixpoints?

I haven't seen any proposed rules of how that would work.

I tried the inductive definition of IsTrunc, and Coq accepts it in the modified form below, but it seems quite awkward to work with.

Cumulative Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| istrunc_iscontr : Contr_internal A -> IsTrunc_internal A minus_two
| istrunc_succ : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).

Existing Class IsTrunc_internal.

Notation IsTrunc n A := (IsTrunc_internal A n).

It's not just that you need to apply constructors, but that you need to go backwards. For example, we define Contr A to be IsTrunc (-2) A, but then one needs to prove that Contr A is equivalent to Contr_internal A. And when given a hypothesis of the form IsTrunc n.+1 A, when you do induction on it, you need to handle the istrunc_iscontr constructor somehow. The following helps:

Scheme IsTrunc_internal_ind := Induction for IsTrunc_internal Sort Type.
Scheme IsTrunc_internal_rec := Minimality for IsTrunc_internal Sort Type.
Definition IsTrunc_internal_rect := IsTrunc_internal_ind.

Definition IsTrunc_unfolded (n : trunc_index) (A : Type)
  := match n with
    | minus_two => Contr_internal A
    | n.+1 => forall x y : A, IsTrunc n (x = y)
    end.

Definition istrunc_unfold (n : trunc_index) (A : Type)
  : IsTrunc n A -> IsTrunc_unfolded n A.
Proof.
  intros [istr|k istr]; exact istr.
Defined.

Definition isequiv_istrunc_unfold (n : trunc_index) (A : Type)
  : IsEquiv (istrunc_unfold n A).
Proof.
  simple refine (Build_IsEquiv _ _ (istrunc_unfold n A) _ _ _ _).
  - destruct n; constructor; assumption.
  - destruct n; reflexivity.
  - intros [istr|k istr]; reflexivity.
  - intros [istr|k istr]; reflexivity.
Defined.

Definition equiv_istrunc_unfold (n : trunc_index) (A : Type)
  := Build_Equiv _ _ _  (isequiv_istrunc_unfold n A).

I also put primes on the constructors of Contr_internal and did:

Definition center (A : Type) {H : Contr A} : A := @center' A (istrunc_unfold _ _ H).
Definition contr {A : Type} {H : Contr A} (y : A) : center A = y := @contr' A (istrunc_unfold _ _ H) y.

But even with these, it's annoying to work with. E.g. the last result in Contractible.v needs to use that ap of an equivalence is an equivalence, but that currently comes later. It wouldn't be hard to flip the dependency between Contractible.v and Equivalences.v to handle this, but I suspect that we'd continue to find it annoying to work with.

We could also rid of Contr_internal and incorporate it in the definition of IsTrunc:

Cumulative Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| istrunc_iscontr : (center : A) -> (forall y : A, center = y) -> IsTrunc_internal A minus_two
| istrunc_succ : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).

Then there would only need to be one definition of center and contr.

For example, we define Contr A to be IsTrunc (-2) A, but then one needs to prove that Contr A is equivalent to Contr_internal A. And when given a hypothesis of the form IsTrunc n.+1 A, when you do induction on it, you need to handle the istrunc_iscontr constructor somehow.

Sure, but don't we only need to do that once? Once we've proven the relevant equivalences, we can just apply those lemmas and tactics.

In general, I've come more and more to believe in the principle that whenever possible types should be canonical, not things that compute definitionally, because this makes it easier to match against them. For instance, mightn't an inductive IsTrunc simplify some of the problems with typeclass inference? We have the comment that

We prefer to reason about [IsTrunc (S n) A] rather than [IsTrunc n (@paths A a b)]

but if IsTrunc is canonical there would be no difficulty with this: IsTrunc (S n) A doesn't reduce to anything, we just have to apply a tactic or lemma to use it (e.g. istrunc_intro x y rather than intros x y).

@mikeshulman You're probably right that with appropriate tactics, using the inductive definition would be fairly painless. But it would probably require many small changes throughout the entire library to do the conversion, so it might be a bit of work.

Another observation is that with my sample code above, we essentially have both definitions. IsTrunc is the inductive one, and IsTrunc_unfolded is essentially the fixpoint one, except that it goes via IsTrunc in the inductive step. Theorems would be stated using IsTrunc and proved using IsTrunc_unfolded, and we'd be frequently converting back and forth. Except for the benefit of cumulativity, it would seem cleaner to just use one definition. One of the things I've learned is that if you can get things to work out definitionally, it really simplifies things in many cases!

It seems to me that the only time we'd actually need to transfer explicitly across that equivalence would be in proving that IsTrunc is a proposition (and we might be able to just do that by hand without introducing IsTrunc_internal at all). Once we know that, it seems to me that in further proofs we'd only need to use the constructors of IsTrunc and their inverses.

@jdchristensen Are you happy with this being merged?

No, let's not merge this yet. If the WIP on making IsTrunc inductive pans out, then the last commit here will need to be undone. Also, I plan to see if I can make similar improvements to Nat.

I rebased, removed the universe variables added to proofs of IsHSet, etc., removed universe variables in Empty, improved the simple_induction tactic (so you don't have to do intro n first, which should also make the proof term smaller), added simple_induction' (with autogenerated IH name), and removed the universe variables from Spaces/Nat/*. I think this is ready to merge once this batch of changes has been reviewed.

I wonder if we can shadow induction everywhere and define it as simple_induction.